FDL - Step of Proof: inv_image_ind

Step of Proof: inv_image_ind_tp

12,41

Inference at * 1 1
Iof proof for Lemma inv image ind tp:

1. T : Type
2. r : T

3. S : Type
4. f : S

T
5. WellFnd{i}(T;x,y.r(x,y))

P:(S

). (

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j))

{

n:S. P(n)}

by ((((Unfold `guard` 0)

CollapseTHEN (UnivCD))

)

CollapseTHENA ((Auto_aux (first_nat 1:n

C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))

C1:

C1: 6. P : S

C1: 7.

j:S. (

k:S. r(f(k),f(j))

P(k))

P(j)

C1: 8. n : S

C1:

P(n)

Definitions t T, {T}, x(s), P Q, x:A. B(x), x(s1,s2),